#######################################################
# Example of PingPong Game using FRTDEVS players
# Author: moonho.hwang@gmail.com
#   Date: Oct.19.2011
#######################################################
from XSY.DEVS.FRTDEVS import *
from XSY.DEVS.CoupledDEVS import *
from XSY.DEVS.SimEngine import SimEngine
from XSY.DEVS.VeriEngine import VeriEngine

class Process(FRTDEVS):
   def __init__(m, n, tl, tu, parent=None):
      '''constructor'''
      FRTDEVS.__init__(m, n, parent) 
      m.tl, m.tu = tl, tu
      m.work = None
      m.addInputPorts('?in')
      m.addOutputPorts('!out', '!out_signal')

   def delta_0(m):
      '''initial state'''
      m.phase = 'IS' # initial send 

   def rv_tau(m):
      '''lifespan range function'''
      if m.phase == 'IS':
         return float(0)
      elif m.phase == 'S':
         return TInterval(m.tl,m.tu) # 
      else:
         return float('inf') # 

   def delta_x(m, x):
      '''external transition function'''
      if x.port == m.IP['?in'] and m.phase == 'W':
         m.phase = 'S'
         m.work = x.value
         return True
      else:
         return False
               
   def delta_y(m):
      '''output and internal transition function'''
      if m.phase == 'S':
         y = PortValue(m.OP["!out"], m.work)
         m.phase = 'W'
         m.work = None
         return y
      elif m.phase == 'IS':
         m.phase = 'W'
         y = PortValue(m.OP["!out_signal"])
         return y

   def get_state(m):
      '''get the state'''
      return m.phase, m.work

   def set_state(m, s):
      '''set the state as s'''
      m.phase, m.work = s
 
def runSimulation(md):
   engine = SimEngine(md)

   #---- setting StepByStep and DES simulation only ----
   engine.StepByStep = True
   engine.sfactor = float('inf')
   #----------------------------------------------------
   engine.runInteractiveMenu()
############################################################################################################
def checkLiveness(KDAG):
   '''check if sc if kernel DAG is alive'''
   for k in KDAG.V:
      sc = KDAG.kv[k] # for each vertex cv in KDAG.V
      if len(sc)>1: # multiple vertex in it
         model_E = {} # check model n true for having 'E' state
         model_S = {} # check model n true for having 'S' state
         for v in sc: # for each vertex v in sc
            for n in v.s: # for each model n in v
               if n not in model_E: model_E[n] = False # initialization
               if n not in model_S: model_S[n] = False # initialization
               if v.s[n][0][0] == 'W': # the  first [0]: discrete state s, [1] lifetime ts (see XSY\DEVS\ReachGen.py)
	                               # the second [0]: phase (see get_state(m))
                  model_E[n] = True 
               elif v.s[n][0][0] == 'S':# the first [0]: discrete state s, [1] lifetime ts (see XSY\DEVS\ReachGen.py)
	                                # the second [0]: phase (see get_state(m)) 
                  model_S[n] = True
         all_meet = True
         for n in model_E:
            if not(model_E[n] and model_S[n]):
               all_meet = False
               break
         if all_meet:
            return True
   return False # there is a kernel vertex satisfying the condition     

def runVerification(md):
   '''run a verification thread'''
   X = [ PortValue(md.IP['?in'],True) ] # no input needs to be tested.
     
   VE = VeriEngine(md, X, None, checkLiveness)
   VE.runtimeInteractiveMenu()

if __name__ == '__main__':
   md = Process('Proc', 10, 20)
   c = True
   while c:
      s = raw_input('[s]im, [v]eri, e[x]it>')
      if s == 's' or s == 'sim': 
         runSimulation(md)
      elif s == 'v' or s == 'veri':
         runVerification(md)
      elif s == 'x' or s == 'exit':
         c = False
      else:
         print('%s is an invalid input!'%s)
      
   print "good bye~!" 
